Bug fix

Closes: #38

Description

I've totally removed the old typing system and reworked it in something new:

• There is no more layering of types in the internal representation, we trust the elaboration between parsing terms and internal terms to handle this stuff. This is less confusing when working with types in the internal syntax.
• Types are not embedded into terms / formulas anymore: only metavariables get their type. This makes the API of terms/formulas more easily maintainable as we don't need to worry about types.
• The typing system itself has been simplified to make it more maintainable: we don't check well-formedness of contexts anymore as it's useless.
• Moreover, there's only one global environment. This makes it easy to interpret a type statement: simply add the pair (name, type) to the global env using the only exposed function that does that.
• The global environment can be queried with type instantiations, and lets the user do the error management in these types using option types.
• Overall, the typing system yields better errors and has a way better debug environment using a high-level and a low-level debugger.
• Added MixedSubstitution, which stores both term and type substitutions. Adapted the destructive proof search to make use of it. DMT is not fully supported yet, but I think the update is straightforward. Non-destructive search does not support mixed substitutions (as an aside, maybe we should cleanup the non destructive version, it doesn't work anyway so we could simply return errors saying this isn't implemented yet or simply remove the option to do non-destructive search).
• Cleaned-up some old functions out of the proof search.
• Disabled context printing of typed problems in Rocq/LambdaPi output as they were mostly useless anyway. I'm planning to fix it when taking care of Syntax error in Rocq output due to illegal character in skolem symbols / types #52

PR dependencies

• Cleanup: replace *FormList by Lib.List[Form] #46
• Debuggers for a more fine-grained debug output #49
• Fix test-suite script to avoid returning if exit code isn't specified #55

Test-suite update

• added basic TFF1 file to check that type metas are properly substituted in proofs test-suite/proofs/tf1_basic_thm.p
• added basic TFF1 file to check that skolemized type variables are properly instantiated in proofs test-suite/proofs/tf1_basic_thm-2.p
• added TFF1 file that should fail at typechecking that allowed me to find a bug in the generic parallel library and the function calls test-suite/bugs/bug_53-1.p
• added elaboration tests test-suite/basic/test-typing-elab-n.p to check the ad-hoc polymorphism of defined arithmetic functions and the edge case of quotients